es:ES, P:(E), R:(EE).
single-thread-generator{i:l}(es;P;R)
 (e, e':E. (R(e,e'))  (P(e) & P(e')))
 (a, b, e:E. (R(a,e) & R(b,e))  (P(e) & P(a) & P(b))  (a = b)) 

latex

Definitions	s = t, <a, b>, P  Q, P & Q, x:A  B(x), x(s), f(a), single-thread-generator{i:l}(es;P;R), x:AB(x), E, x:A. B(x), , Type, t  T, ES, A c B, P  Q, left + right, x f y, P  Q, P  Q, R^+, R!, A, False
Lemmas	rel-rel-plus, generated-thread-properties2, event system wf, es-E wf, single-thread-generator wf